If a functor represents a given profunctor, then the action of the functor on morphisms is determined by the action of the profunctor and the representation isomorphism.
This theorem can make it easier to define certain adjoint functors, and is also implicit in type theory where type connectives are presentation of functors, but the action on morphisms is derivable rather than primitive.
Let ⇸ be a profunctor, i.e., a functor from and a functor that represents it by a natural isomorphism . Then the action of on morphisms is determined by by the formula:
or the following composite acting on :
Since the action of the functor on morphisms is determined by the data of a representation of a profunctor, we can even define the functor by giving that data. Crucially though, what does it mean for to be natural if we have not yet defined the action of ? It turns out that it is sufficient to require naturality in only. Furthermore, can be recovered from its action on the identity by the Yoneda lemma.
A right functor presentation from to consists of
satisfying
Given a profunctor ⇸, right functor presentations representing are in bijection with functors with a natural isomorphism .
Given a right functor presentation , we can define a functor that represents by extending to act on morphisms by . Then the functoriality of and naturality of and follow from the above equalities.
Given a functor representing , the universal morphism is defined as in the Yoneda lemma: .
A right functor presentation consists of exactly the data that define a negative type in type theory. The introduction rule of the presentation, unsurprisingly corresponds to the introduction rule in the type theory. The universal morphism corresponds to the (0 or more) elimination rules that are collected into . Left-naturality corresponds to the definition of substitution for the introduction rule. The isomorphism property corresponds to the and equalities.
This theorem is usually not explicitly invoked in initiality theorems for type theories, but gives an explanation for why the “dogma” of introduction and elimination rules is so effective in practice.
whose action is defined as . Then the universal property of the product functor is encapsulated in the natural isomorphism . By the Yoneda lemma, the inverse of can be reconstructed from its action on the identity, which in this case gives us the two projections: .
Then, by the above theorem, the action of on functions is equal to:
A similar theorem, but for presenting adjoint functors without defining first is given (and generalized to the internal setting) in
Last revised on February 19, 2024 at 17:05:25. See the history of this page for a list of all contributions to it.